%PONGAMOS EN COMENTARIOS PARA CADA AUX EN QUÉ EJERCICIO SE USAN. NOS VA A SERVIR
% PARA ORDENARLOS AL FINAL

%Interseccion de dos grupos a y b, devuelve una lista de tipo [T] con los
% elementos que esten presentes en ambos

\section{Auxiliares mas usados}

\subsection{Originales}

%Chequea que no haya repetidos en una misma cadena.
\begin{aux}{sinRepetidos}{a: [T]}{Bool}{
	(\forall i,j \selec [0 .. \longitud{a})), i\not=j) a_i \not= a_j}
\end{aux}

%Chequea que haya un gateway con el numero dado
\begin{aux}{hayGatewayConNro}{nro: \ent, gs:[Gateway]}{Bool}{
	(\exists g \selec gs)numero(g) == nro}
\end{aux}

%Chequea que no haya espacios en una cadena dada
\begin{aux}{sinEspacios}{s: String}{Bool}{
	(\forall i \selec [0 .. \longitud{s})) s_i \not= \!' \ \ \!'}
\end{aux}

%SE USA POR PRIMERA VEZ EN EL 9
\begin{aux}{insterseccion}{a,b: [T]}{[T]}{
	\comp{x}{x \selec a, x \in b} }
\end{aux}

\subsection{Generales}


\begin{aux}{dameIndiceProxPregunta}{t: Trivia, u: Usuario}{[\ent]}{\\
	\comp{i}{ i \selec [0..\longitud{preguntas(t)}), proxPregunta(t) ==
	preguntas(t)_i }
}
\end{aux}

%SE USA POR PRIMERA VEZ EN EL 6
\begin{aux}{cantidadMensajes}{t:Trivia, u:Usuario}{\ent}{\\
ifThenElse(u \in ganadores(t),\longitud {preguntas(t)},cab(dameIndiceProxPregunta(t,u))+1)}
\end{aux}

%En el 10
\aux{dameTrivia}{g: Gateway, k: Keyword}{Trivia}{
	 \comp{h}{h \selec trivias(g), k \in keywords(h)}_0 
}

\begin{aux}{cascabel}{l: [T]}{T}{
	cab(\comp{ l_{\longitud{l}-1-i} }{i \selec [0..\longitud{l})})
}
\end{aux}

\begin{aux}{sacarRepetidos}{l:[T]}{[T]}{
 \comp {l_i}{i \selec [0..\longitud {l}),l_i \notin l_{[0..i)} }}
\end{aux}

\medskip

%SE USA POR PRIMERA VEZ EN EL 4

\begin{aux}{losDemasMismosPuntajes}{t,preT: Trivia, u: usuario}{Bool}{
	\\ (\forall j \selec participantes(t), j \not= u) (puntajeAcumulado(t,j) ==
	puntajeAcumulado(preT,j))
	}
\end{aux}

\begin{aux}{losDemasMismasPreguntas}{t,preT: Trivia, u: usuario}{Bool}{
	\\ (\forall j \selec participantes(t), j \not= u, j \not\in ganadores(t) )
	(proxPregunta(t,j) == proxPregunta(preT,j)) }
\end{aux}

% Chicos, modifiqu� este auxiliar (lo part� en 2) para que no se indefina. Es mi
% primer commit desde casa xD. Y le saqu� una parte que creo que no hac�a falta
% poner

\begin{aux}{loDemasNoCambiaT}{t,preT: Trivia}{Bool}{
	mismos(keywords(t),keywords(preT))\\ \ylogico
	mismos(participantes(t),participantes(preT)) \ylogico
	preguntas(t)==preguntas(preT)
}
\end{aux}

\begin{aux}{loDemasNoCambiaG}{g,preG: Gateway}{Bool}{
	(numero(g) == numero(preG)) \\ \ylogico (mismos(comandos(g) , comandos(preG)))
}
\end{aux}



\subsection{Auxiliar damePalabras y asociados}
%SE USA POR PRIMERA VEZ EN EL 5 CREO
\begin{aux}{damePalabras}{s: String}{[String]}{
	\comp{\comp{s[i]}{i \selec indicesPalabras(s)_j}}{j \selec [0..\longitud
	{indicesPalabras(s)}]}}
\end{aux}

\begin{aux}{indicesPalabras}{s: String}{[[\ent]]}{
	escaleras(indexarLetras(s))}
\end{aux}

%IDEM DAMEPALABRAS
\begin{aux}{escaleras}{l: [\ent]}{[[\ent]]}{
	\comp{l_{[dameSaltos(l)[i]..[dameSaltos(l)[i+1])}]}{i \selec [0..\longitud
	{dameSaltos(l)}-1)}
}
\end{aux}


%IDEM DAMEPALABRAS
\begin{aux}{dameSaltos}{l: [\ent]}{[\ent]}{
	0:\comp{i}{i \selec [1..\longitud{l}), l_{i-1} \not = l_i-1} \masmas [\longitud
	{l}]
}
\end{aux}

%IDEM DAMEPALABRAS
\begin{aux}{indexarLetras}{s: String}{[\ent]}{
	\comp{i}{i \selec [0..\longitud{s}), s_i \in ['a'..'z'] \masmas ['A'..'Z']
	\masmas ['0'..'9']}
}
\end{aux}




%['h'o'l'i'i' 'j'i'j'i' 'o']
%indexarletras[0,1,2,3,4,6,7,8,9,11]
%damesaltos[0,5,9,10]
%escalera[[0,1,2,3,4],[6,7,8,9],[11]]
%damepalabras[['h'o'l'i'i']['j'i'j'i']['o']]


%PONGAMOS EN COMENTARIOS PARA CADA AUX EN QUÉ EJERCICIO SE USAN. NOS VA A SERVIR
% PARA ORDENARLOS AL FINAL